Lemma `inv\_image\_ind\_tp`